es:ES, C, T:Type, In:AbsInterface(:(:C  C)  T). abs-S   CCE 

latex

Definitions

abs-S , AbsInterface(A), A c B, , e  X, t.1, x.A(x), X(e), E, EqDecider(T), EOrderAxioms(E; pred?; info), kind(e), type List, Msg(M), , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , P & Q, x:A  B(x), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), IdLnk, constant_function(f;A;B), P  Q, s = t, <a, b>, loc(e), A, b, first(e), suptype(S; T), Type, left + right, S  T, Top, x:A.B(x), Void, Unit, SWellFounded(R(x;y)), pred!(e;e'), x:A. B(x), x:AB(x), , Id, EState(T), f(a), t  T, ES

Lemmas

event system wf, unit wf, top wf, first wf, assert wf, not wf, constant function wf, EState wf, IdLnk wf, kindcase wf, Knd wf, rationals wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, loc wf, kind wf, Id wf, EOrderAxioms wf, deq wf, es-E wf, es-interface-val wf, pi1 wf, es-is-interface wf